KEVM performance:

There is a major slowdown in engagement proofs as a result of this PR. A setUp function that was passing in 6m39s with master is passing in 15m17s with this branch.

I think that we might need to construct a more representative test suite.

I've removed the data in this comment as I've been running with an incorrect branch, sorry for the spam.

I've run the testkontrolEscrowLockUnlockTest.setUp with master and this branch combined with two other SMT-related PRs (#4040 and #4038), and the results are:

This proof seems to be special in the sense that it does not branch a single time and always stays in Booster, hence this change introduces a slowdown, as we start calling Z3 at the beginning of every execute request.

It is not clear to me at that point why the slowdown is so massive.

With cdce88c the runtime of testkontrolEscrowLockUnlockTest.setUp is back to 7m 34s. The problem was that we were checking the constraints with Z3 after every rewrite step (in simplifyP).

Just in case this could be useful. For me, the SAT checking points are:

• for prelude, once, at the very beginning of the execution;
• for the path constraint:
  • at the very beginning of the execution; and
  • when ensures adds something to it.

I don't think there is a need to make additional checks at branching points, because there are already checks in place that Prelude /\ G /\ P and Prelude /\ G /\ !P are SAT. If those are SAT, then also G and Prelude are SAT, and if those are both Unsat, we signal vacuous anyway presumably.

Even if we cut both Prelude and G, if the cut is correct then the above reasoning still holds, because irrelevant extensions cannot make UNSAT what was SAT unless they make either the Prelude or G itself UNSAT, but our initial checks, ensures checks, and branching point checks would have eliminated those cases already.

To measure the effect of this PR, I am running:

export GHCRTS=-N16
GHCRTS='' kontrol build --require test/kontrol/lido-lemmas.k --module-import VetoSignallingTest:LIDO-LEMMAS --verbose --regen --rekompile
kontrol prove --verbose --smt-timeout 64000 --match-test "VetoSignallingTest.testVetoSignallingInvariantsArePreserved" --max-depth 100000 --max-iterations 10000 --smt-retry-limit 0 --max-frontier-parallel 6 --kore-rpc-command='kore-rpc-booster --no-post-exec-simplify' --no-log-rewrites --no-fail-fast --no-counterexample-information --maintenance-rate 64 --assume-defined

I am running using commit e951c3171e189d25fa45679d7a93700ecc55ae6a of Kontrol (this will be master tomorrow), which has K version 7.1.112 (master now).

With HB version 0.1.67, which comes with that version of K (it's a bit behind, isn't it?), the result is as follows:

APRProof: test%kontrol%VetoSignallingTest.testVetoSignallingInvariantsArePreserved(uint256,uint256,uint256):0
    status: ProofStatus.PASSED
    admitted: False
    nodes: 568
    pending: 0
    failing: 0
    vacuous: 24
    stuck: 0
    terminal: 28
    refuted: 0
    bounded: 0
    execution time: 17m 19s

which is actually a record-breaking time by ~4 minutes.

Using HB from this branch, commit 5862b7029a89774de786e0b098e8808386bf3338, the result is as follows:

APRProof: test%kontrol%VetoSignallingTest.testVetoSignallingInvariantsArePreserved(uint256,uint256,uint256):0
    status: ProofStatus.PASSED
    admitted: False
    nodes: 568
    pending: 0
    failing: 0
    vacuous: 24
    stuck: 0
    terminal: 28
    refuted: 0
    bounded: 0
    execution time: 48m 13s

and it is clear that having a SAT check at the start of each request causes a substantial overhead. Here, it means that ~560 extra checks were made with respect to the master version, and as the execution progressed, they got harder and harder, resulting in a 30m 54s overhead.

TL; DR: This does not look good for real-world proofs. I think we need to really understand do we want this at all, that is, what is the worst that could happen if we actually started a request from an UNSAT state in the booster.

Thanks @PetarMax!

I'd like to re-iterate on the ask to upstream this test, perhaps partially, as to KEVM as a claim, so that we can run is as part of out performance measurement.

Regarding having an RPC parameter to turn the initial constraints check off: we actually already have one we could use. It is the "assume-state-defined" parameter of the "execute" endpoint which we introduced for Kore purposes and which is unused in Booster. We can skip the initial pattern check if this parameter is set by the client. @jberthold @goodlyrottenapple what do you guys think?